$\forall$$A$, $B$:Type, $b$:$A$+$B$, $f$, $L_{1}$, $L_{2}$:Top.
\\[0ex]map($f$;Case $b$ of inl($a$) $\Rightarrow$ $L_{1}$($a$) ; inr($a$) $\Rightarrow$ $L_{2}$($a$))
\\[0ex]$\sim$
\\[0ex]Case $b$ of inl($a$) $\Rightarrow$ map($f$;$L_{1}$($a$)) ; inr($a$) $\Rightarrow$ map($f$;$L_{2}$($a$))